Rename homo to ∙-homo in Algebra.Morphism.Structures#2464
Rename homo to ∙-homo in Algebra.Morphism.Structures#2464jamesmckinna wants to merge 18 commits intoagda:masterfrom
homo to ∙-homo in Algebra.Morphism.Structures#2464Conversation
JacquesCarette
left a comment
JacquesCarette
left a comment
There was a problem hiding this comment.
Looks good to me - but isn't this a breaking change?
I forget (or: have never properly understood?!) whether changing (field) names via deprecation is |
|
Yes, unfortunately it is an unavoidable breaking change. |
|
Thanks @gallais but I'd been waiting to merge until we had a clean |
MatthewDaggitt
left a comment
MatthewDaggitt
left a comment
There was a problem hiding this comment.
Otherwise looks good.
| * In `Algebra.Morphism.Structures`: | ||
| ```agda | ||
| homo ↦ ∙-homo | ||
| ``` |
There was a problem hiding this comment.
This unfortunately is in the wrong section of the CHANGELOG, as it's not a deprecated name. Instead it's a breaking change to the name.
There was a problem hiding this comment.
Yes, that's a good catch. Sorry not to have revisited this recently... will fix.
There was a problem hiding this comment.
Now done... but there is still a WARNING_ON_USE deprecation warning in Algebra.Morphism.Structures.IsMagmaHomomorphism associated with the copy of the old name. Does that not also merit an entry in the Deprecated names section? If not, will remove! Please advise
4 participants
Fixes #2458
NB: the warning-on-usage does not seem to be correctly triggering when reference to
homois made inrenamingdirectives, nor in actual usage? UPDATED: A known, but not-yet-fixed, Agda bug. Grrrr.UPDATED: TODO
CHANGELOGonly after the v2.x milestone/release cycle converges